es:ES, i, x:Id, T:Type, L:Knd List. @i only events in L change   x : T  Prop 

latex

Definitions	x:A. B(x), t  T, Prop, @i only events in L change   x : T, A & B, P  Q, x. t(x), x(s)
Lemmas	alle-at wf, Id wf, es-loc wf, es-after wf, es-vartype wf, es-when wf, Knd wf, event system wf